;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mrotate.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")
(require "mdatagenerators.lisp")

; Module responsible for testing the rotate module
(module TRotate
  (import IRotate)
  (import IDataGenerators)
  (import Ibmptree)
  (import Iavltree)
  
  (include-book "doublecheck" :dir :teachpacks) 
  (include-book "testing" :dir :teachpacks)
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; DATA GENERATORS
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
 
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))

  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; Check-expect tests
 
  (check-expect (rotate nil 90) nil)
  
  (check-expect (rotate-90 (make-bmp-tree 
                            (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                        0 0 0 0 0 0 3 0 0 0 3)
                                  (list 0 0 (list 1 1 1)) 
                                  (list 0 1 (list 2 2 2))
                                  (list 0 2 (list 3 3 3)) 
                                  (list 1 0 (list 4 4 4))
                                  (list 1 1 (list 5 5 5)) 
                                  (list 1 2 (list 0 0 0))
                                  (list 2 0 (list 7 7 7)) 
                                  (list 2 1 (list 8 8 8))
                                  (list 2 2 (list 9 9 9)))))
                (list 3
                      0
                      (list 2 1 (list 4 4 4) (list 1 0 (list 7 7 7) nil nil) (list 1 2 (list 1 1 1) nil nil))
                      (list 1 -1 (list 1 -1 (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 3 0 0 0 3) nil nil) nil nil)
                      (list 2
                            1
                            (list 2 1 (list 5 5 5) (list 1 0 (list 8 8 8) nil nil) (list 1 2 (list 2 2 2) nil nil))
                            nil
                            (list 1 2 (list 2 1 (list 0 0 0) (list 1 0 (list 9 9 9) nil nil) (list 1 2 (list 3 3 3) 
                                                                                                   nil nil)) nil nil))))
  (check-expect (rotate-180 (make-bmp-tree 
                             (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                         0 0 0 0 0 0 3 0 0 0 3)
                                   (list 0 0 (list 1 1 1)) 
                                   (list 0 1 (list 2 2 2))
                                   (list 0 2 (list 3 3 3)) 
                                   (list 1 0 (list 4 4 4))
                                   (list 1 1 (list 5 5 5)) 
                                   (list 1 2 (list 0 0 0))
                                   (list 2 0 (list 7 7 7)) 
                                   (list 2 1 (list 8 8 8))
                                   (list 2 2 (list 9 9 9)))))
                (list 3
                      0
                      (list 2 1 (list 8 8 8) (list 1 0 (list 9 9 9) nil nil) (list 1 2 (list 7 7 7) nil nil))
                      (list 1 -1 (list 1 -1 (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 3 0 0 0 3) nil nil) nil nil)
                      (list 2
                            1
                            (list 2 1 (list 5 5 5) (list 1 0 (list 0 0 0) nil nil) (list 1 2 (list 4 4 4) nil nil))
                            nil
                            (list 1 2 (list 2 1 (list 2 2 2) (list 1 0 (list 3 3 3) nil nil) (list 1 2 (list 1 1 1) nil nil)) nil nil))))
  
  (check-expect (rotate-270 (make-bmp-tree 
                             (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                         0 0 0 0 0 0 3 0 0 0 3)
                                   (list 0 0 (list 1 1 1)) 
                                   (list 0 1 (list 2 2 2))
                                   (list 0 2 (list 3 3 3)) 
                                   (list 1 0 (list 4 4 4))
                                   (list 1 1 (list 5 5 5)) 
                                   (list 1 2 (list 0 0 0))
                                   (list 2 0 (list 7 7 7)) 
                                   (list 2 1 (list 8 8 8))
                                   (list 2 2 (list 9 9 9)))))
                (list 3
                      0
                      (list 2 1 (list 4 4 4) (list 1 0 (list 1 1 1) nil nil) (list 1 2 (list 7 7 7) nil nil))
                      (list 1 -1 (list 1 -1 (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 3 0 0 0 3) nil nil) nil nil)
                      (list 2
                            1
                            (list 2 1 (list 5 5 5) (list 1 0 (list 2 2 2) nil nil) (list 1 2 (list 8 8 8) nil nil))
                            nil
                            (list 1 2 (list 2 1 (list 0 0 0) (list 1 0 (list 3 3 3) nil nil) (list 1 2 (list 9 9 9) nil nil)) nil nil))))
  

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; Property definitions
  
  ; verifies that rotate-90 switches the dimensions
  (defproperty rotate-90-switches-dimensions :repeat 10
    (oldtr :value (random-bitmap 5 5)
     newtr :value (rotate-90 oldtr)
     neww :value (car (get-dimensions newtr))
     newh :value (cdr (get-dimensions newtr))
     oldw :value (car (get-dimensions oldtr))
     oldh :value (cdr (get-dimensions oldtr)))
     (and (equal neww oldh) (equal newh oldw)))
  
  ; verifies that rotate-180 preserves the dimensions
  (defproperty rotate-180-preserves-dimensions :repeat 10
    (oldtr :value (random-bitmap 5 5)
     newtr :value (rotate-180 oldtr)
     neww :value (car (get-dimensions newtr))
     newh :value (cdr (get-dimensions newtr))
     oldw :value (car (get-dimensions oldtr))
     oldh :value (cdr (get-dimensions oldtr)))
     (and (equal neww oldw) (equal newh oldh)))
  
  ; verifies that rotate-270 switches the dimensions
  (defproperty rotate-270-switches-dimensions :repeat 10
    (oldtr :value (random-bitmap 5 5)
     newtr :value (rotate-270 oldtr)
     neww :value (car (get-dimensions newtr))
     newh :value (cdr (get-dimensions newtr))
     oldw :value (car (get-dimensions oldtr))
     oldh :value (cdr (get-dimensions oldtr)))
     (and (equal neww oldh) (equal newh oldw)))
 
  ; verifies that rotate returns a tree
  (defproperty rotate-returns-tree-prp :repeat 10
    (tr    :value (random-bitmap 5 5)
     angle :value (random-case 90 180 270))
    (bmp-tree? (rotate tr angle)))
  
  ; verifies that rotate-90 returns a tree
  (defproperty rotate-90-returns-tree-prp :repeat 10
    (tr    :value (random-bitmap 5 5))
    (bmp-tree? (rotate-90 tr)))
  
  ; verifies that rotate-180 returns a tree
  (defproperty rotate-180-returns-tree-prp :repeat 10
    (tr    :value (random-bitmap 5 5))
    (bmp-tree? (rotate-180 tr)))
  
  ; verifies that rotate-270 returns a tree
  (defproperty rotate-270-returns-tree-prp :repeat 10
    (tr    :value (random-bitmap 5 5))
    (bmp-tree? (rotate-270 tr)))
  
  ; verifies that rotate-90-helper returns a tree
  (defproperty rotate-90-helper-returns-tree-prp :repeat 10
    (tr :value (random-bitmap 5 5)
     oldwidth :value 5
     newtr :value (insert-header (empty-bmp-tree) (get-header tr))
     xcurr :value 0
     ycurr :value 0
     xmax :value 5
     ymax :value 5)
    (bmp-tree? (rotate-90-helper tr oldwidth newtr xcurr xmax ycurr ymax (get-row tr 0))))
  
  ; verifies that rotate-180-helper returns a tree
  (defproperty rotate-180-helper-returns-tree-prp :repeat 10
    (oldtr :value (random-bitmap 5 5)
     height :value 5
     newtr :value (insert-header (empty-bmp-tree) (get-header oldtr))
     xcurr :value 0
     ycurr :value 0
     xmax :value 5
     ymax :value 5)
    (bmp-tree? (rotate-180-helper oldtr height newtr xcurr xmax ycurr ymax (get-row oldtr 0))))
  
  ; verifies that rotate-270-helper returns a tree
  (defproperty rotate-270-helper-returns-tree-prp :repeat 10
    (oldtr :value (random-bitmap 5 5)
     newtr :value (insert-header (empty-bmp-tree) (get-header oldtr))
     xcurr :value 0
     ycurr :value 0
     xmax :value 5
     ymax :value 5)
    (bmp-tree? (rotate-270-helper oldtr newtr xcurr xmax ycurr ymax (get-row oldtr 0))))  
  )

(link RTRotate (Mavltree Mbmptree Mdatagenerators MRotate TRotate))
(invoke RTRotate)